$\forall$$A$:Type, $d$:DS($A$), $a$:$A$, $x$, $y$:dstype($A$; $d$; $a$). $x$ = $y$ $\in$ $\mathbb{B}$